Search for: All records

Scientific software is, by its very nature, complex. It is mathematical and highly optimized which makes it prone to subtle bugs not as easily detected by traditional testing. We outline how symbolic execution can be used to write tests similar to traditional unit tests while providing stronger verification guarantees and apply this methodology to a sparse matrix algorithm. 

Earth System Models (ESMs) are critical for understanding past climates and projecting future scenarios. However, the complexity of these models, which include large code bases, a wide community of developers, and diverse computational platforms, poses significant challenges for software quality assurance. The increasing adoption of GPUs and heterogeneous architectures further complicates verification efforts. Traditional verification methods often rely on bitwise reproducibility, which is not always feasible, particularly under new compilers or hardware. Manual expert evaluation, on the other hand, is subjective and time-consuming. Formal methods offer a mathematically rigorous alternative, yet their application in ESM development has been limited due to the lack of climate model-specific representations and tools. Here, we advocate for the broader adoption of formal methods in climate modeling. In particular, we identify key aspects of ESMs that are well suited to formal specification and introduce abstraction approaches for a tailored framework. To demonstrate this approach, we present a case study using CIVL model checker to formally verify a bug fix in an ocean mixing parameterization scheme. Our goal is to develop accessible, domain-specific formal tools that enhance model confidence and support more efficient and reliable ESM development. 

Intestinal microbiota confers susceptibility to diet-induced obesity yet many probiotic species that synthesize tryptophan (trp) actually attenuate this effect, however the underlying mechanisms are unclear. We monocolonized germ-free (GF) mice with a widely consumed probiotic Lacticaseibacillus rhamnosus GG (LGG) under trp-free or -sufficient dietary conditions. We obtained untargeted metabolomics from the mouse feces and serum using liquid chromatography-mass spectrometry and obtained intestinal transcriptomic profiles via bulk-RNA sequencing. When comparing LGG-monocolonized mice with GF mice, we found a synergy between LGG and dietary trp in markedly promoting the transcriptome of fatty acid metabolism and -oxidation. Upregulation was specific and was not observed in transcriptomes of trp-fed conventional mice and mice monocolonized with Ruminococcus gnavus. Metabolomics showed that fecal and serum metabolites were also modified by LGG-host-trp interaction. We developed an R-Script based MEtabolome-TRanscriptome Correlation Analysis (METRCA) algorithm and uncovered LGG- and trp-dependent metabolites that were positively or negatively correlated with fatty acid metabolism and -oxidation gene networks. This high throughput metabolome-transcriptome correlation strategy can be used in similar investigations to reveal potential interactions between specific metabolites and functional or disease-related transcriptomic networks.